FDL - Nuprl Definition : ma-sub

Nuprl Definition : ma-sub

0,22

postcript pdf

M2
== 1of(M1)

1of(M2) & 1of(2of(M1))

1of(2of(M2))
== & 1of(2of(2of(M1)))

1of(2of(2of(M2)))
== & & 1of(2of(2of(2of(M1))))

1of(2of(2of(2of(M2))))
== & & 1of(2of(2of(2of(2of(M1)))))

1of(2of(2of(2of(2of(M2)))))
== & & 1of(2of(2of(2of(2of(2of(M1))))))

1of(2of(2of(2of(2of(2of(M2))))))
== & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))

1of(2of(2of(2of(2of(2of(2of(M2)))))))
== & & 1of(2of(2of(2of(2of(2of(2of(2of(M1))))))))

1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))
== & & 1of(2of(2of(2of(2of(2of(2of(2of(2of(M1)))))))))

1of(2of(2of(2of(2of(2of(2of(2of(2of(
== & & 1of(2of(2of(2of(2of(2of(2of(2of(2of(M1)))))))))

1of(M2)))))))))
== & & 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
== & & 1of(M1))))))))))

1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2))))))))))
== & & 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(
== & & 1of(M1)))))))))))

1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))))

latex

clarification:

ma-sub{i:l}
ma-sub(M1; M2)
== fpf-sub(Id; x.Type{i}; IdDeq; 1of(M1); 1of(M2))
== & fpf-sub(Knd; x.Type{i}; KindDeq; 1of(2of(M1)); 1of(2of(M2)))
== & fpf-sub(Id; x.fpf-cap(1of(M2);IdDeq;x;Void); IdDeq; 1of(2of(2of(M1))); 1of(2of(2of(M2))))
== & & fpf-sub(Id;
== & & fpf-sub(a.(State(1of(M2))

fpf-cap(1of(2of(M2));KindDeq;locl(a);Top)

Prop{i});
== & & fpf-sub(IdDeq;
== & & fpf-sub(1of(2of(2of(2of(M1))));
== & & fpf-sub(1of(2of(2of(2of(M2)))))
== & & fpf-sub((Knd

Id);
== & & fpf-sub(kx.(State(1of(M2))

Valtype(1of(2of(M2));1of(kx))

== & & fpf-sub(fpf-cap(1of(M2);IdDeq;2of(kx);Void));
== & & fpf-sub(product-deq(Knd;Id;KindDeq;IdDeq);
== & & fpf-sub(1of(2of(2of(2of(2of(M1)))));
== & & fpf-sub(1of(2of(2of(2of(2of(M2))))))
== & & fpf-sub((Knd

IdLnk);
== & & fpf-sub(kl.((tg:Id
== & & fpf-sub(kl.((

(State(1of(M2))

Valtype(1of(2of(M2));1of(kl))

== & & fpf-sub(kl.((

((fpf-cap(1of(2of(M2));KindDeq;rcv(2of(kl),tg);Void) List))) List);
== & & fpf-sub(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);
== & & fpf-sub(1of(2of(2of(2of(2of(2of(M1))))));
== & & fpf-sub(1of(2of(2of(2of(2of(2of(M2)))))))
== & & fpf-sub(Id;
== & & fpf-sub(x.(Knd List);
== & & fpf-sub(IdDeq;
== & & fpf-sub(1of(2of(2of(2of(2of(2of(2of(M1)))))));
== & & fpf-sub(1of(2of(2of(2of(2of(2of(2of(M2))))))))
== & & fpf-sub((IdLnk

Id);
== & & fpf-sub(ltg.(Knd List);
== & & fpf-sub(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);
== & & fpf-sub(1of(2of(2of(2of(2of(2of(2of(2of(M1))))))));
== & & fpf-sub(1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))
== & & fpf-sub(Knd;
== & & fpf-sub(k.(Id List);
== & & fpf-sub(KindDeq;
== & & fpf-sub(1of(2of(2of(2of(2of(2of(2of(2of(2of(M1)))))))));
== & & fpf-sub(1of(2of(2of(2of(2of(2of(2of(2of(2of(M2))))))))))
== & & fpf-sub(Knd;
== & & fpf-sub(k.(IdLnk List);
== & & fpf-sub(KindDeq;
== & & fpf-sub(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M1))))))))));
== & & fpf-sub(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))))
== & & fpf-sub(Id;
== & & fpf-sub(x.(Knd List);
== & & fpf-sub(IdDeq;
== & & fpf-sub(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M1)))))))))));
== & & fpf-sub(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M2))))))))))))

latex

Definitions A & B, Type, locl(a), Top, Prop, State(ds), x:AB(x), Valtype(da;k), f(x)?z, rcv(l,tg), Void, x:AB(x), product-deq(A;B;a;b), IdLnkDeq, P & Q, IdLnk, KindDeq, f g, Id, type List, Knd, IdDeq, 1of(t), 2of(t)

FDL editor aliases ma-sub

origin

Definitions	A & B, Type, locl(a), Top, Prop, State(ds), x:AB(x), Valtype(da;k), f(x)?z, rcv(l,tg), Void, x:AB(x), product-deq(A;B;a;b), IdLnkDeq, P & Q, IdLnk, KindDeq, f g, Id, type List, Knd, IdDeq, 1of(t), 2of(t)
FDL editor aliases	ma-sub